Arbiters are widely used in electronic systems such as microprocessors and interconnects. Arbiters restrict access to shared resources when the number of requests exceeds the maximum number of requests that can be satisfied concurrently. Arbiters may select the order of access to a shared resource, when several requests are co-pending. Efficient arbiters may require that the arbitration function is performed quickly as long decision time may add to the memory access time and may also increase the effective memory cycle time. Efficient arbiters may be bug-prone. See, for example, David J. Kinniment, Synchronization and Arbitration in Digital Systems, PROC. IEE, Vol. 123, No 10, October 1976 961-966, which is hereby incorporated by reference.
Arbiters are widely used in both synchronous and asynchronous contexts.
One concern in verification of an arbiter design is checking for starvation. Starvation is a special case of liveness properties, in which any request must eventually be granted. Liveness properties are often computationally hard to verify even on medium-sized designs. To alleviate this, it is common to check for starvation by replacing liveness properties with bounded properties—“request will be granted within N cycles”, for some constant N. If a bounded property passes, it implies the correctness of the original liveness property while providing insight into the performance aspects of the arbiter. Even so, the sheer size of industrial arbiters may preclude an exhaustive analysis of the bounded property.